(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)
Rewrite Strategy: FULL
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
times(x, s(y)) →+ plus(times(x, y), x)
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [y / s(y)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
times(x, 0') → 0'
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)
S is empty.
Rewrite Strategy: FULL
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
TRS:
Rules:
times(x, 0') → 0'
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)
Types:
times :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
0' :: 0':s:zero:true:false
s :: 0':s:zero:true:false → 0':s:zero:true:false
plus :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
if :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
gt :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
not :: 0':s:zero:true:false → 0':s:zero:true:false
id :: 0':s:zero:true:false → 0':s:zero:true:false
zero :: 0':s:zero:true:false
true :: 0':s:zero:true:false
false :: 0':s:zero:true:false
hole_0':s:zero:true:false1_0 :: 0':s:zero:true:false
gen_0':s:zero:true:false2_0 :: Nat → 0':s:zero:true:false
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
times,
plus,
gtThey will be analysed ascendingly in the following order:
plus < times
gt < plus
(8) Obligation:
TRS:
Rules:
times(
x,
0') →
0'times(
x,
s(
y)) →
plus(
times(
x,
y),
x)
plus(
s(
x),
s(
y)) →
s(
s(
plus(
if(
gt(
x,
y),
x,
y),
if(
not(
gt(
x,
y)),
id(
x),
id(
y)))))
plus(
s(
x),
x) →
plus(
if(
gt(
x,
x),
id(
x),
id(
x)),
s(
x))
plus(
zero,
y) →
yplus(
id(
x),
s(
y)) →
s(
plus(
x,
if(
gt(
s(
y),
y),
y,
s(
y))))
id(
x) →
xif(
true,
x,
y) →
xif(
false,
x,
y) →
ynot(
x) →
if(
x,
false,
true)
gt(
s(
x),
zero) →
truegt(
zero,
y) →
falsegt(
s(
x),
s(
y)) →
gt(
x,
y)
Types:
times :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
0' :: 0':s:zero:true:false
s :: 0':s:zero:true:false → 0':s:zero:true:false
plus :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
if :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
gt :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
not :: 0':s:zero:true:false → 0':s:zero:true:false
id :: 0':s:zero:true:false → 0':s:zero:true:false
zero :: 0':s:zero:true:false
true :: 0':s:zero:true:false
false :: 0':s:zero:true:false
hole_0':s:zero:true:false1_0 :: 0':s:zero:true:false
gen_0':s:zero:true:false2_0 :: Nat → 0':s:zero:true:false
Generator Equations:
gen_0':s:zero:true:false2_0(0) ⇔ 0'
gen_0':s:zero:true:false2_0(+(x, 1)) ⇔ s(gen_0':s:zero:true:false2_0(x))
The following defined symbols remain to be analysed:
gt, times, plus
They will be analysed ascendingly in the following order:
plus < times
gt < plus
(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol gt.
(10) Obligation:
TRS:
Rules:
times(
x,
0') →
0'times(
x,
s(
y)) →
plus(
times(
x,
y),
x)
plus(
s(
x),
s(
y)) →
s(
s(
plus(
if(
gt(
x,
y),
x,
y),
if(
not(
gt(
x,
y)),
id(
x),
id(
y)))))
plus(
s(
x),
x) →
plus(
if(
gt(
x,
x),
id(
x),
id(
x)),
s(
x))
plus(
zero,
y) →
yplus(
id(
x),
s(
y)) →
s(
plus(
x,
if(
gt(
s(
y),
y),
y,
s(
y))))
id(
x) →
xif(
true,
x,
y) →
xif(
false,
x,
y) →
ynot(
x) →
if(
x,
false,
true)
gt(
s(
x),
zero) →
truegt(
zero,
y) →
falsegt(
s(
x),
s(
y)) →
gt(
x,
y)
Types:
times :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
0' :: 0':s:zero:true:false
s :: 0':s:zero:true:false → 0':s:zero:true:false
plus :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
if :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
gt :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
not :: 0':s:zero:true:false → 0':s:zero:true:false
id :: 0':s:zero:true:false → 0':s:zero:true:false
zero :: 0':s:zero:true:false
true :: 0':s:zero:true:false
false :: 0':s:zero:true:false
hole_0':s:zero:true:false1_0 :: 0':s:zero:true:false
gen_0':s:zero:true:false2_0 :: Nat → 0':s:zero:true:false
Generator Equations:
gen_0':s:zero:true:false2_0(0) ⇔ 0'
gen_0':s:zero:true:false2_0(+(x, 1)) ⇔ s(gen_0':s:zero:true:false2_0(x))
The following defined symbols remain to be analysed:
plus, times
They will be analysed ascendingly in the following order:
plus < times
(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol plus.
(12) Obligation:
TRS:
Rules:
times(
x,
0') →
0'times(
x,
s(
y)) →
plus(
times(
x,
y),
x)
plus(
s(
x),
s(
y)) →
s(
s(
plus(
if(
gt(
x,
y),
x,
y),
if(
not(
gt(
x,
y)),
id(
x),
id(
y)))))
plus(
s(
x),
x) →
plus(
if(
gt(
x,
x),
id(
x),
id(
x)),
s(
x))
plus(
zero,
y) →
yplus(
id(
x),
s(
y)) →
s(
plus(
x,
if(
gt(
s(
y),
y),
y,
s(
y))))
id(
x) →
xif(
true,
x,
y) →
xif(
false,
x,
y) →
ynot(
x) →
if(
x,
false,
true)
gt(
s(
x),
zero) →
truegt(
zero,
y) →
falsegt(
s(
x),
s(
y)) →
gt(
x,
y)
Types:
times :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
0' :: 0':s:zero:true:false
s :: 0':s:zero:true:false → 0':s:zero:true:false
plus :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
if :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
gt :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
not :: 0':s:zero:true:false → 0':s:zero:true:false
id :: 0':s:zero:true:false → 0':s:zero:true:false
zero :: 0':s:zero:true:false
true :: 0':s:zero:true:false
false :: 0':s:zero:true:false
hole_0':s:zero:true:false1_0 :: 0':s:zero:true:false
gen_0':s:zero:true:false2_0 :: Nat → 0':s:zero:true:false
Generator Equations:
gen_0':s:zero:true:false2_0(0) ⇔ 0'
gen_0':s:zero:true:false2_0(+(x, 1)) ⇔ s(gen_0':s:zero:true:false2_0(x))
The following defined symbols remain to be analysed:
times
(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol times.
(14) Obligation:
TRS:
Rules:
times(
x,
0') →
0'times(
x,
s(
y)) →
plus(
times(
x,
y),
x)
plus(
s(
x),
s(
y)) →
s(
s(
plus(
if(
gt(
x,
y),
x,
y),
if(
not(
gt(
x,
y)),
id(
x),
id(
y)))))
plus(
s(
x),
x) →
plus(
if(
gt(
x,
x),
id(
x),
id(
x)),
s(
x))
plus(
zero,
y) →
yplus(
id(
x),
s(
y)) →
s(
plus(
x,
if(
gt(
s(
y),
y),
y,
s(
y))))
id(
x) →
xif(
true,
x,
y) →
xif(
false,
x,
y) →
ynot(
x) →
if(
x,
false,
true)
gt(
s(
x),
zero) →
truegt(
zero,
y) →
falsegt(
s(
x),
s(
y)) →
gt(
x,
y)
Types:
times :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
0' :: 0':s:zero:true:false
s :: 0':s:zero:true:false → 0':s:zero:true:false
plus :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
if :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
gt :: 0':s:zero:true:false → 0':s:zero:true:false → 0':s:zero:true:false
not :: 0':s:zero:true:false → 0':s:zero:true:false
id :: 0':s:zero:true:false → 0':s:zero:true:false
zero :: 0':s:zero:true:false
true :: 0':s:zero:true:false
false :: 0':s:zero:true:false
hole_0':s:zero:true:false1_0 :: 0':s:zero:true:false
gen_0':s:zero:true:false2_0 :: Nat → 0':s:zero:true:false
Generator Equations:
gen_0':s:zero:true:false2_0(0) ⇔ 0'
gen_0':s:zero:true:false2_0(+(x, 1)) ⇔ s(gen_0':s:zero:true:false2_0(x))
No more defined symbols left to analyse.